0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 188 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 263 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 124 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 1 ms)
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 QReductionProof (⇔, 0 ms)
↳33 QDP
↳34 QDPSizeChangeProof (⇔, 0 ms)
↳35 YES
↳36 PiDP
↳37 UsableRulesProof (⇔, 0 ms)
↳38 PiDP
↳39 PiDPToQDPProof (⇒, 0 ms)
↳40 QDP
↳41 QDPSizeChangeProof (⇔, 0 ms)
↳42 YES
↳43 PiDP
↳44 UsableRulesProof (⇔, 0 ms)
↳45 PiDP
↳46 PiDPToQDPProof (⇒, 0 ms)
↳47 QDP
↳48 QDPQMonotonicMRRProof (⇔, 947 ms)
↳49 QDP
↳50 DependencyGraphProof (⇔, 0 ms)
↳51 TRUE
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U10_GA(X1, X2, X3, X4, splitA_in_gaa(X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITA_IN_GAA(X3, X5, X6)
SPLITA_IN_GAA(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U1_GAA(X1, X2, X3, X4, X5, splitA_in_gaa(X3, X4, X5))
SPLITA_IN_GAA(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → SPLITA_IN_GAA(X3, X4, X5)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U11_GA(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U12_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X5), X7))
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X5), X7)
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U13_GA(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U14_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X2, X6), X8))
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → MERGESORTB_IN_GA(.(X2, X6), X8)
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U15_GA(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U15_GA(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U16_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U15_GA(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → MERGEC_IN_GGA(X7, X8, X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U2_GGA(X1, X2, X3, X4, X5, leD_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LED_IN_GG(X1, X3)
LED_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, leD_in_gg(X1, X2))
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U3_GGA(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
U3_GGA(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U4_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(X2, .(X3, X4), X5))
U3_GGA(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U5_GGA(X1, X2, X3, X4, X5, gtE_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTE_IN_GG(X1, X3)
GTE_IN_GG(s(X1), s(X2)) → U9_GG(X1, X2, gtE_in_gg(X1, X2))
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U6_GGA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U7_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X1, X2), X4, X5))
U6_GGA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U10_GA(X1, X2, X3, X4, splitA_in_gaa(X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITA_IN_GAA(X3, X5, X6)
SPLITA_IN_GAA(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U1_GAA(X1, X2, X3, X4, X5, splitA_in_gaa(X3, X4, X5))
SPLITA_IN_GAA(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → SPLITA_IN_GAA(X3, X4, X5)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U11_GA(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U12_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X5), X7))
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X5), X7)
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U13_GA(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U14_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X2, X6), X8))
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → MERGESORTB_IN_GA(.(X2, X6), X8)
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U15_GA(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U15_GA(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U16_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U15_GA(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → MERGEC_IN_GGA(X7, X8, X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U2_GGA(X1, X2, X3, X4, X5, leD_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LED_IN_GG(X1, X3)
LED_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, leD_in_gg(X1, X2))
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U3_GGA(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
U3_GGA(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U4_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(X2, .(X3, X4), X5))
U3_GGA(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U5_GGA(X1, X2, X3, X4, X5, gtE_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTE_IN_GG(X1, X3)
GTE_IN_GG(s(X1), s(X2)) → U9_GG(X1, X2, gtE_in_gg(X1, X2))
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U6_GGA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U7_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X1, X2), X4, X5))
U6_GGA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
GTE_IN_GG(s(X1), s(X2)) → GTE_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
LED_IN_GG(s(X1), s(X2)) → LED_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U3_GGA(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
U3_GGA(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U6_GGA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U3_GGA(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
U3_GGA(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U6_GGA(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U3_GGA(X1, X2, X3, X4, lecD_in_gg(X1, X3))
U3_GGA(X1, X2, X3, X4, lecD_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U6_GGA(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecD_in_gg(x0, x1)
gtcE_in_gg(x0, x1)
U27_gg(x0, x1, x2)
U28_gg(x0, x1, x2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U3_GGA(X1, X2, X3, X4, lecD_in_gg(X1, X3))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
POL(.(x1, x2)) = 1 + 2·x1 + x2
POL(0) = 0
POL(MERGEC_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U27_gg(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U28_gg(x1, x2, x3)) = x1 + x2 + x3
POL(U3_GGA(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + 2·x3 + 2·x4 + x5
POL(U6_GGA(x1, x2, x3, x4, x5)) = 2 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5
POL(gtcE_in_gg(x1, x2)) = 1 + x1 + x2
POL(gtcE_out_gg(x1, x2)) = x1 + x2
POL(lecD_in_gg(x1, x2)) = 2·x1 + 2·x2
POL(lecD_out_gg(x1, x2)) = 2·x1 + 2·x2
POL(s(x1)) = 2·x1
U3_GGA(X1, X2, X3, X4, lecD_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U6_GGA(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecD_in_gg(x0, x1)
gtcE_in_gg(x0, x1)
U27_gg(x0, x1, x2)
U28_gg(x0, x1, x2)
U6_GGA(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U6_GGA(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecD_in_gg(x0, x1)
gtcE_in_gg(x0, x1)
U27_gg(x0, x1, x2)
U28_gg(x0, x1, x2)
U6_GGA(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U6_GGA(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
lecD_in_gg(x0, x1)
gtcE_in_gg(x0, x1)
U27_gg(x0, x1, x2)
U28_gg(x0, x1, x2)
lecD_in_gg(x0, x1)
U27_gg(x0, x1, x2)
U6_GGA(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U6_GGA(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
gtcE_in_gg(x0, x1)
U28_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
SPLITA_IN_GAA(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → SPLITA_IN_GAA(X3, X4, X5)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
SPLITA_IN_GAA(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → SPLITA_IN_GAA(X3, X4, X5)
SPLITA_IN_GAA(.(X1, .(X2, X3))) → SPLITA_IN_GAA(X3)
From the DPs we obtained the following set of size-change graphs:
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U11_GA(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X5), X7)
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U13_GA(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → MERGESORTB_IN_GA(.(X2, X6), X8)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U11_GA(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X5), X7)
U11_GA(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U13_GA(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U13_GA(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → MERGESORTB_IN_GA(.(X2, X6), X8)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, []), .(X1, []), []) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5)) → U18_gaa(X1, X2, X3, X4, X5, splitcA_in_gaa(X3, X4, X5))
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U19_ga(X1, X2, X3, X4, splitcA_in_gaa(X3, X5, X6))
U18_gaa(X1, X2, X3, X4, X5, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
U19_ga(X1, X2, X3, X4, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X4, X6, mergesortcB_in_ga(.(X1, X5), X7))
U20_ga(X1, X2, X3, X4, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X4, X7, mergesortcB_in_ga(.(X2, X6), X8))
U21_ga(X1, X2, X3, X4, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U22_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U23_gga(X1, X2, X3, X4, X5, lecD_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U25_gga(X1, X2, X3, X4, X5, gtcE_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, X5, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
U25_gga(X1, X2, X3, X4, X5, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U24_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U26_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U11_GA(X1, X2, X3, splitcA_in_gaa(X3))
U11_GA(X1, X2, X3, splitcA_out_gaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X5))
U11_GA(X1, X2, X3, splitcA_out_gaa(X3, X5, X6)) → U13_GA(X1, X2, X3, X6, mergesortcB_in_ga(.(X1, X5)))
U13_GA(X1, X2, X3, X6, mergesortcB_out_ga(.(X1, X5), X7)) → MERGESORTB_IN_GA(.(X2, X6))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, [])) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3))) → U18_gaa(X1, X2, X3, splitcA_in_gaa(X3))
mergesortcB_in_ga(.(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3))) → U19_ga(X1, X2, X3, splitcA_in_gaa(X3))
U18_gaa(X1, X2, X3, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
U19_ga(X1, X2, X3, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X6, mergesortcB_in_ga(.(X1, X5)))
U20_ga(X1, X2, X3, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X7, mergesortcB_in_ga(.(X2, X6)))
U21_ga(X1, X2, X3, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U22_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U23_gga(X1, X2, X3, X4, lecD_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U25_gga(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U25_gga(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U24_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U26_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcA_in_gaa(x0)
mergesortcB_in_ga(x0)
U18_gaa(x0, x1, x2, x3)
U19_ga(x0, x1, x2, x3)
U20_ga(x0, x1, x2, x3, x4)
U21_ga(x0, x1, x2, x3, x4)
U22_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U23_gga(x0, x1, x2, x3, x4)
U25_gga(x0, x1, x2, x3, x4)
lecD_in_gg(x0, x1)
U24_gga(x0, x1, x2, x3, x4)
gtcE_in_gg(x0, x1)
U26_gga(x0, x1, x2, x3, x4)
U27_gg(x0, x1, x2)
U28_gg(x0, x1, x2)
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U11_GA(X1, X2, X3, splitcA_in_gaa(X3))
POL(.(x1, x2)) = 1 + 2·x2
POL(0) = 0
POL(MERGESORTB_IN_GA(x1)) = x1
POL(U11_GA(x1, x2, x3, x4)) = 1 + 2·x4
POL(U13_GA(x1, x2, x3, x4, x5)) = 1 + 2·x4
POL(U18_gaa(x1, x2, x3, x4)) = 2 + x3 + 2·x4
POL(U19_ga(x1, x2, x3, x4)) = 0
POL(U20_ga(x1, x2, x3, x4, x5)) = 0
POL(U21_ga(x1, x2, x3, x4, x5)) = 0
POL(U22_ga(x1, x2, x3, x4)) = 0
POL(U23_gga(x1, x2, x3, x4, x5)) = 1
POL(U24_gga(x1, x2, x3, x4, x5)) = 0
POL(U25_gga(x1, x2, x3, x4, x5)) = 2·x2 + x4 + 2·x5
POL(U26_gga(x1, x2, x3, x4, x5)) = 2·x2 + x4
POL(U27_gg(x1, x2, x3)) = 0
POL(U28_gg(x1, x2, x3)) = 1
POL([]) = 0
POL(gtcE_in_gg(x1, x2)) = 2
POL(gtcE_out_gg(x1, x2)) = 1
POL(lecD_in_gg(x1, x2)) = 1
POL(lecD_out_gg(x1, x2)) = 2·x1
POL(mergecC_in_gga(x1, x2)) = 1 + x1 + 2·x2
POL(mergecC_out_gga(x1, x2, x3)) = 0
POL(mergesortcB_in_ga(x1)) = 0
POL(mergesortcB_out_ga(x1, x2)) = 0
POL(s(x1)) = 0
POL(splitcA_in_gaa(x1)) = x1
POL(splitcA_out_gaa(x1, x2, x3)) = x2 + x3
U11_GA(X1, X2, X3, splitcA_out_gaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X5))
U11_GA(X1, X2, X3, splitcA_out_gaa(X3, X5, X6)) → U13_GA(X1, X2, X3, X6, mergesortcB_in_ga(.(X1, X5)))
U13_GA(X1, X2, X3, X6, mergesortcB_out_ga(.(X1, X5), X7)) → MERGESORTB_IN_GA(.(X2, X6))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, [])) → splitcA_out_gaa(.(X1, []), .(X1, []), [])
splitcA_in_gaa(.(X1, .(X2, X3))) → U18_gaa(X1, X2, X3, splitcA_in_gaa(X3))
mergesortcB_in_ga(.(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3))) → U19_ga(X1, X2, X3, splitcA_in_gaa(X3))
U18_gaa(X1, X2, X3, splitcA_out_gaa(X3, X4, X5)) → splitcA_out_gaa(.(X1, .(X2, X3)), .(X1, X4), .(X2, X5))
U19_ga(X1, X2, X3, splitcA_out_gaa(X3, X5, X6)) → U20_ga(X1, X2, X3, X6, mergesortcB_in_ga(.(X1, X5)))
U20_ga(X1, X2, X3, X6, mergesortcB_out_ga(.(X1, X5), X7)) → U21_ga(X1, X2, X3, X7, mergesortcB_in_ga(.(X2, X6)))
U21_ga(X1, X2, X3, X7, mergesortcB_out_ga(.(X2, X6), X8)) → U22_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U22_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U23_gga(X1, X2, X3, X4, lecD_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U25_gga(X1, X2, X3, X4, gtcE_in_gg(X1, X3))
U23_gga(X1, X2, X3, X4, lecD_out_gg(X1, X3)) → U24_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U25_gga(X1, X2, X3, X4, gtcE_out_gg(X1, X3)) → U26_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecD_in_gg(s(X1), s(X2)) → U27_gg(X1, X2, lecD_in_gg(X1, X2))
lecD_in_gg(0, s(X1)) → lecD_out_gg(0, s(X1))
lecD_in_gg(0, 0) → lecD_out_gg(0, 0)
U24_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcE_in_gg(s(X1), s(X2)) → U28_gg(X1, X2, gtcE_in_gg(X1, X2))
gtcE_in_gg(s(X1), 0) → gtcE_out_gg(s(X1), 0)
U26_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U27_gg(X1, X2, lecD_out_gg(X1, X2)) → lecD_out_gg(s(X1), s(X2))
U28_gg(X1, X2, gtcE_out_gg(X1, X2)) → gtcE_out_gg(s(X1), s(X2))
splitcA_in_gaa(x0)
mergesortcB_in_ga(x0)
U18_gaa(x0, x1, x2, x3)
U19_ga(x0, x1, x2, x3)
U20_ga(x0, x1, x2, x3, x4)
U21_ga(x0, x1, x2, x3, x4)
U22_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U23_gga(x0, x1, x2, x3, x4)
U25_gga(x0, x1, x2, x3, x4)
lecD_in_gg(x0, x1)
U24_gga(x0, x1, x2, x3, x4)
gtcE_in_gg(x0, x1)
U26_gga(x0, x1, x2, x3, x4)
U27_gg(x0, x1, x2)
U28_gg(x0, x1, x2)